the_es:ES, e:E, l:IdLnk, m:Msg, i:, e1:E.
i<||sends(l;e)||
 m = sends(l;e)[i]
 isrcv(e1)
 lnk(e1) = l
 tag(e1) = mtag(m)  Id
 msgtype(m) = valtype(e1)  Type 

latex

Definitions	t  T, {T}, P  Q, x:A. B(x), SQType(T), IdLnk, s = t, Prop, ||as||, s ~ t, False, A, AB, , {x:A| B(x) }, , x:AB(x), lnk(e), mlnk(m), <a,b>, es-M(es), f(a), Id, Type, x:AB(x), mtag(m), rcvtype(e), msgtype(m), b, b, , isrcv(e), P & Q, P  Q, Unit, left+right, valtype(e), (Msg on l), ES, E, Msg, sends(l;e), a<b, #$n, Void, type List, S  T, l[i], tag(e), haslink(l;m), Msg(M)
Lemmas	Id wf, es-tag wf, es-mtag wf, es-lnk wf, select wf, length wf1, es-Msgl wf, es-sends wf, nat wf, es-Msg wf, es-E wf, event system wf, es-mval wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-isrcv wf, bool wf, bnot wf, not wf, assert wf, es-M wf, IdLnk wf, IdLnk sq